T:Type, R:(TT).
(a, b:T. Dec(R(a,b)))
 (Connex(T;x,y.R(x,y))
  {a, b:T.
  strict_part(x,y.R(x,y);a;b)
   Symmetrize(x,y.R(x,y);a;b)
   strict_part(x,y.R(x,y);b;a)}) 

latex

Up	rel 1, rel 1
Definitions	{T}, t  T, P  Q, P & Q, Symmetrize(x,y.R(x;y);a;b), strict_part(x,y.R(x;y);a;b), P  Q, Connex(T;x,y.R(x;y)), P  Q, x(s1,s2), P  Q, , x:A. B(x), Dec(P)
Lemmas	decidable wf, not wf